0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 88 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 13 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 38 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 6 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 1 ms)
↳27 QDP
↳28 MRRProof (⇔, 26 ms)
↳29 QDP
↳30 PisEmptyProof (⇔, 0 ms)
↳31 YES
permE_in_ga(.(T24, T25), .(T26, T27)) → U4_ga(T24, T25, T26, T27, app1A_in_aaag(X45, T26, X46, T25))
app1A_in_aaag(.(T50, X94), T52, X95, .(T50, T51)) → U1_aaag(T50, X94, T52, X95, T51, app1A_in_aaag(X94, T52, X95, T51))
app1A_in_aaag([], T60, T61, .(T60, T61)) → app1A_out_aaag([], T60, T61, .(T60, T61))
U1_aaag(T50, X94, T52, X95, T51, app1A_out_aaag(X94, T52, X95, T51)) → app1A_out_aaag(.(T50, X94), T52, X95, .(T50, T51))
U4_ga(T24, T25, T26, T27, app1A_out_aaag(X45, T26, X46, T25)) → permE_out_ga(.(T24, T25), .(T26, T27))
permE_in_ga(.(T24, T25), .(T26, T33)) → U5_ga(T24, T25, T26, T33, app1A_in_aaag(T31, T26, T32, T25))
U5_ga(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → U6_ga(T24, T25, T26, T33, app2C_in_ggga(T24, T31, T32, X11))
app2C_in_ggga(T87, T88, T89, .(T87, X153)) → U3_ggga(T87, T88, T89, X153, app2B_in_gga(T88, T89, X153))
app2B_in_gga(.(T105, T106), T107, .(T105, X183)) → U2_gga(T105, T106, T107, X183, app2B_in_gga(T106, T107, X183))
app2B_in_gga([], T113, T113) → app2B_out_gga([], T113, T113)
U2_gga(T105, T106, T107, X183, app2B_out_gga(T106, T107, X183)) → app2B_out_gga(.(T105, T106), T107, .(T105, X183))
U3_ggga(T87, T88, T89, X153, app2B_out_gga(T88, T89, X153)) → app2C_out_ggga(T87, T88, T89, .(T87, X153))
U6_ga(T24, T25, T26, T33, app2C_out_ggga(T24, T31, T32, X11)) → permE_out_ga(.(T24, T25), .(T26, T33))
U5_ga(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → U7_ga(T24, T25, T26, T33, app2C_in_ggga(T24, T31, T32, T65))
U7_ga(T24, T25, T26, T33, app2C_out_ggga(T24, T31, T32, T65)) → U8_ga(T24, T25, T26, T33, permE_in_ga(T65, T33))
permE_in_ga(.(T125, T126), .(T125, T127)) → U9_ga(T125, T126, T127, app2D_in_ga(T126, X11))
app2D_in_ga(T131, T131) → app2D_out_ga(T131, T131)
U9_ga(T125, T126, T127, app2D_out_ga(T126, X11)) → permE_out_ga(.(T125, T126), .(T125, T127))
permE_in_ga(.(T125, T126), .(T125, T127)) → U10_ga(T125, T126, T127, app2D_in_ga(T126, T128))
U10_ga(T125, T126, T127, app2D_out_ga(T126, T128)) → U11_ga(T125, T126, T127, permE_in_ga(T128, T127))
permE_in_ga([], []) → permE_out_ga([], [])
U11_ga(T125, T126, T127, permE_out_ga(T128, T127)) → permE_out_ga(.(T125, T126), .(T125, T127))
U8_ga(T24, T25, T26, T33, permE_out_ga(T65, T33)) → permE_out_ga(.(T24, T25), .(T26, T33))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
permE_in_ga(.(T24, T25), .(T26, T27)) → U4_ga(T24, T25, T26, T27, app1A_in_aaag(X45, T26, X46, T25))
app1A_in_aaag(.(T50, X94), T52, X95, .(T50, T51)) → U1_aaag(T50, X94, T52, X95, T51, app1A_in_aaag(X94, T52, X95, T51))
app1A_in_aaag([], T60, T61, .(T60, T61)) → app1A_out_aaag([], T60, T61, .(T60, T61))
U1_aaag(T50, X94, T52, X95, T51, app1A_out_aaag(X94, T52, X95, T51)) → app1A_out_aaag(.(T50, X94), T52, X95, .(T50, T51))
U4_ga(T24, T25, T26, T27, app1A_out_aaag(X45, T26, X46, T25)) → permE_out_ga(.(T24, T25), .(T26, T27))
permE_in_ga(.(T24, T25), .(T26, T33)) → U5_ga(T24, T25, T26, T33, app1A_in_aaag(T31, T26, T32, T25))
U5_ga(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → U6_ga(T24, T25, T26, T33, app2C_in_ggga(T24, T31, T32, X11))
app2C_in_ggga(T87, T88, T89, .(T87, X153)) → U3_ggga(T87, T88, T89, X153, app2B_in_gga(T88, T89, X153))
app2B_in_gga(.(T105, T106), T107, .(T105, X183)) → U2_gga(T105, T106, T107, X183, app2B_in_gga(T106, T107, X183))
app2B_in_gga([], T113, T113) → app2B_out_gga([], T113, T113)
U2_gga(T105, T106, T107, X183, app2B_out_gga(T106, T107, X183)) → app2B_out_gga(.(T105, T106), T107, .(T105, X183))
U3_ggga(T87, T88, T89, X153, app2B_out_gga(T88, T89, X153)) → app2C_out_ggga(T87, T88, T89, .(T87, X153))
U6_ga(T24, T25, T26, T33, app2C_out_ggga(T24, T31, T32, X11)) → permE_out_ga(.(T24, T25), .(T26, T33))
U5_ga(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → U7_ga(T24, T25, T26, T33, app2C_in_ggga(T24, T31, T32, T65))
U7_ga(T24, T25, T26, T33, app2C_out_ggga(T24, T31, T32, T65)) → U8_ga(T24, T25, T26, T33, permE_in_ga(T65, T33))
permE_in_ga(.(T125, T126), .(T125, T127)) → U9_ga(T125, T126, T127, app2D_in_ga(T126, X11))
app2D_in_ga(T131, T131) → app2D_out_ga(T131, T131)
U9_ga(T125, T126, T127, app2D_out_ga(T126, X11)) → permE_out_ga(.(T125, T126), .(T125, T127))
permE_in_ga(.(T125, T126), .(T125, T127)) → U10_ga(T125, T126, T127, app2D_in_ga(T126, T128))
U10_ga(T125, T126, T127, app2D_out_ga(T126, T128)) → U11_ga(T125, T126, T127, permE_in_ga(T128, T127))
permE_in_ga([], []) → permE_out_ga([], [])
U11_ga(T125, T126, T127, permE_out_ga(T128, T127)) → permE_out_ga(.(T125, T126), .(T125, T127))
U8_ga(T24, T25, T26, T33, permE_out_ga(T65, T33)) → permE_out_ga(.(T24, T25), .(T26, T33))
PERME_IN_GA(.(T24, T25), .(T26, T27)) → U4_GA(T24, T25, T26, T27, app1A_in_aaag(X45, T26, X46, T25))
PERME_IN_GA(.(T24, T25), .(T26, T27)) → APP1A_IN_AAAG(X45, T26, X46, T25)
APP1A_IN_AAAG(.(T50, X94), T52, X95, .(T50, T51)) → U1_AAAG(T50, X94, T52, X95, T51, app1A_in_aaag(X94, T52, X95, T51))
APP1A_IN_AAAG(.(T50, X94), T52, X95, .(T50, T51)) → APP1A_IN_AAAG(X94, T52, X95, T51)
PERME_IN_GA(.(T24, T25), .(T26, T33)) → U5_GA(T24, T25, T26, T33, app1A_in_aaag(T31, T26, T32, T25))
U5_GA(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → U6_GA(T24, T25, T26, T33, app2C_in_ggga(T24, T31, T32, X11))
U5_GA(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → APP2C_IN_GGGA(T24, T31, T32, X11)
APP2C_IN_GGGA(T87, T88, T89, .(T87, X153)) → U3_GGGA(T87, T88, T89, X153, app2B_in_gga(T88, T89, X153))
APP2C_IN_GGGA(T87, T88, T89, .(T87, X153)) → APP2B_IN_GGA(T88, T89, X153)
APP2B_IN_GGA(.(T105, T106), T107, .(T105, X183)) → U2_GGA(T105, T106, T107, X183, app2B_in_gga(T106, T107, X183))
APP2B_IN_GGA(.(T105, T106), T107, .(T105, X183)) → APP2B_IN_GGA(T106, T107, X183)
U5_GA(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → U7_GA(T24, T25, T26, T33, app2C_in_ggga(T24, T31, T32, T65))
U7_GA(T24, T25, T26, T33, app2C_out_ggga(T24, T31, T32, T65)) → U8_GA(T24, T25, T26, T33, permE_in_ga(T65, T33))
U7_GA(T24, T25, T26, T33, app2C_out_ggga(T24, T31, T32, T65)) → PERME_IN_GA(T65, T33)
PERME_IN_GA(.(T125, T126), .(T125, T127)) → U9_GA(T125, T126, T127, app2D_in_ga(T126, X11))
PERME_IN_GA(.(T125, T126), .(T125, T127)) → APP2D_IN_GA(T126, X11)
PERME_IN_GA(.(T125, T126), .(T125, T127)) → U10_GA(T125, T126, T127, app2D_in_ga(T126, T128))
U10_GA(T125, T126, T127, app2D_out_ga(T126, T128)) → U11_GA(T125, T126, T127, permE_in_ga(T128, T127))
U10_GA(T125, T126, T127, app2D_out_ga(T126, T128)) → PERME_IN_GA(T128, T127)
permE_in_ga(.(T24, T25), .(T26, T27)) → U4_ga(T24, T25, T26, T27, app1A_in_aaag(X45, T26, X46, T25))
app1A_in_aaag(.(T50, X94), T52, X95, .(T50, T51)) → U1_aaag(T50, X94, T52, X95, T51, app1A_in_aaag(X94, T52, X95, T51))
app1A_in_aaag([], T60, T61, .(T60, T61)) → app1A_out_aaag([], T60, T61, .(T60, T61))
U1_aaag(T50, X94, T52, X95, T51, app1A_out_aaag(X94, T52, X95, T51)) → app1A_out_aaag(.(T50, X94), T52, X95, .(T50, T51))
U4_ga(T24, T25, T26, T27, app1A_out_aaag(X45, T26, X46, T25)) → permE_out_ga(.(T24, T25), .(T26, T27))
permE_in_ga(.(T24, T25), .(T26, T33)) → U5_ga(T24, T25, T26, T33, app1A_in_aaag(T31, T26, T32, T25))
U5_ga(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → U6_ga(T24, T25, T26, T33, app2C_in_ggga(T24, T31, T32, X11))
app2C_in_ggga(T87, T88, T89, .(T87, X153)) → U3_ggga(T87, T88, T89, X153, app2B_in_gga(T88, T89, X153))
app2B_in_gga(.(T105, T106), T107, .(T105, X183)) → U2_gga(T105, T106, T107, X183, app2B_in_gga(T106, T107, X183))
app2B_in_gga([], T113, T113) → app2B_out_gga([], T113, T113)
U2_gga(T105, T106, T107, X183, app2B_out_gga(T106, T107, X183)) → app2B_out_gga(.(T105, T106), T107, .(T105, X183))
U3_ggga(T87, T88, T89, X153, app2B_out_gga(T88, T89, X153)) → app2C_out_ggga(T87, T88, T89, .(T87, X153))
U6_ga(T24, T25, T26, T33, app2C_out_ggga(T24, T31, T32, X11)) → permE_out_ga(.(T24, T25), .(T26, T33))
U5_ga(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → U7_ga(T24, T25, T26, T33, app2C_in_ggga(T24, T31, T32, T65))
U7_ga(T24, T25, T26, T33, app2C_out_ggga(T24, T31, T32, T65)) → U8_ga(T24, T25, T26, T33, permE_in_ga(T65, T33))
permE_in_ga(.(T125, T126), .(T125, T127)) → U9_ga(T125, T126, T127, app2D_in_ga(T126, X11))
app2D_in_ga(T131, T131) → app2D_out_ga(T131, T131)
U9_ga(T125, T126, T127, app2D_out_ga(T126, X11)) → permE_out_ga(.(T125, T126), .(T125, T127))
permE_in_ga(.(T125, T126), .(T125, T127)) → U10_ga(T125, T126, T127, app2D_in_ga(T126, T128))
U10_ga(T125, T126, T127, app2D_out_ga(T126, T128)) → U11_ga(T125, T126, T127, permE_in_ga(T128, T127))
permE_in_ga([], []) → permE_out_ga([], [])
U11_ga(T125, T126, T127, permE_out_ga(T128, T127)) → permE_out_ga(.(T125, T126), .(T125, T127))
U8_ga(T24, T25, T26, T33, permE_out_ga(T65, T33)) → permE_out_ga(.(T24, T25), .(T26, T33))
PERME_IN_GA(.(T24, T25), .(T26, T27)) → U4_GA(T24, T25, T26, T27, app1A_in_aaag(X45, T26, X46, T25))
PERME_IN_GA(.(T24, T25), .(T26, T27)) → APP1A_IN_AAAG(X45, T26, X46, T25)
APP1A_IN_AAAG(.(T50, X94), T52, X95, .(T50, T51)) → U1_AAAG(T50, X94, T52, X95, T51, app1A_in_aaag(X94, T52, X95, T51))
APP1A_IN_AAAG(.(T50, X94), T52, X95, .(T50, T51)) → APP1A_IN_AAAG(X94, T52, X95, T51)
PERME_IN_GA(.(T24, T25), .(T26, T33)) → U5_GA(T24, T25, T26, T33, app1A_in_aaag(T31, T26, T32, T25))
U5_GA(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → U6_GA(T24, T25, T26, T33, app2C_in_ggga(T24, T31, T32, X11))
U5_GA(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → APP2C_IN_GGGA(T24, T31, T32, X11)
APP2C_IN_GGGA(T87, T88, T89, .(T87, X153)) → U3_GGGA(T87, T88, T89, X153, app2B_in_gga(T88, T89, X153))
APP2C_IN_GGGA(T87, T88, T89, .(T87, X153)) → APP2B_IN_GGA(T88, T89, X153)
APP2B_IN_GGA(.(T105, T106), T107, .(T105, X183)) → U2_GGA(T105, T106, T107, X183, app2B_in_gga(T106, T107, X183))
APP2B_IN_GGA(.(T105, T106), T107, .(T105, X183)) → APP2B_IN_GGA(T106, T107, X183)
U5_GA(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → U7_GA(T24, T25, T26, T33, app2C_in_ggga(T24, T31, T32, T65))
U7_GA(T24, T25, T26, T33, app2C_out_ggga(T24, T31, T32, T65)) → U8_GA(T24, T25, T26, T33, permE_in_ga(T65, T33))
U7_GA(T24, T25, T26, T33, app2C_out_ggga(T24, T31, T32, T65)) → PERME_IN_GA(T65, T33)
PERME_IN_GA(.(T125, T126), .(T125, T127)) → U9_GA(T125, T126, T127, app2D_in_ga(T126, X11))
PERME_IN_GA(.(T125, T126), .(T125, T127)) → APP2D_IN_GA(T126, X11)
PERME_IN_GA(.(T125, T126), .(T125, T127)) → U10_GA(T125, T126, T127, app2D_in_ga(T126, T128))
U10_GA(T125, T126, T127, app2D_out_ga(T126, T128)) → U11_GA(T125, T126, T127, permE_in_ga(T128, T127))
U10_GA(T125, T126, T127, app2D_out_ga(T126, T128)) → PERME_IN_GA(T128, T127)
permE_in_ga(.(T24, T25), .(T26, T27)) → U4_ga(T24, T25, T26, T27, app1A_in_aaag(X45, T26, X46, T25))
app1A_in_aaag(.(T50, X94), T52, X95, .(T50, T51)) → U1_aaag(T50, X94, T52, X95, T51, app1A_in_aaag(X94, T52, X95, T51))
app1A_in_aaag([], T60, T61, .(T60, T61)) → app1A_out_aaag([], T60, T61, .(T60, T61))
U1_aaag(T50, X94, T52, X95, T51, app1A_out_aaag(X94, T52, X95, T51)) → app1A_out_aaag(.(T50, X94), T52, X95, .(T50, T51))
U4_ga(T24, T25, T26, T27, app1A_out_aaag(X45, T26, X46, T25)) → permE_out_ga(.(T24, T25), .(T26, T27))
permE_in_ga(.(T24, T25), .(T26, T33)) → U5_ga(T24, T25, T26, T33, app1A_in_aaag(T31, T26, T32, T25))
U5_ga(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → U6_ga(T24, T25, T26, T33, app2C_in_ggga(T24, T31, T32, X11))
app2C_in_ggga(T87, T88, T89, .(T87, X153)) → U3_ggga(T87, T88, T89, X153, app2B_in_gga(T88, T89, X153))
app2B_in_gga(.(T105, T106), T107, .(T105, X183)) → U2_gga(T105, T106, T107, X183, app2B_in_gga(T106, T107, X183))
app2B_in_gga([], T113, T113) → app2B_out_gga([], T113, T113)
U2_gga(T105, T106, T107, X183, app2B_out_gga(T106, T107, X183)) → app2B_out_gga(.(T105, T106), T107, .(T105, X183))
U3_ggga(T87, T88, T89, X153, app2B_out_gga(T88, T89, X153)) → app2C_out_ggga(T87, T88, T89, .(T87, X153))
U6_ga(T24, T25, T26, T33, app2C_out_ggga(T24, T31, T32, X11)) → permE_out_ga(.(T24, T25), .(T26, T33))
U5_ga(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → U7_ga(T24, T25, T26, T33, app2C_in_ggga(T24, T31, T32, T65))
U7_ga(T24, T25, T26, T33, app2C_out_ggga(T24, T31, T32, T65)) → U8_ga(T24, T25, T26, T33, permE_in_ga(T65, T33))
permE_in_ga(.(T125, T126), .(T125, T127)) → U9_ga(T125, T126, T127, app2D_in_ga(T126, X11))
app2D_in_ga(T131, T131) → app2D_out_ga(T131, T131)
U9_ga(T125, T126, T127, app2D_out_ga(T126, X11)) → permE_out_ga(.(T125, T126), .(T125, T127))
permE_in_ga(.(T125, T126), .(T125, T127)) → U10_ga(T125, T126, T127, app2D_in_ga(T126, T128))
U10_ga(T125, T126, T127, app2D_out_ga(T126, T128)) → U11_ga(T125, T126, T127, permE_in_ga(T128, T127))
permE_in_ga([], []) → permE_out_ga([], [])
U11_ga(T125, T126, T127, permE_out_ga(T128, T127)) → permE_out_ga(.(T125, T126), .(T125, T127))
U8_ga(T24, T25, T26, T33, permE_out_ga(T65, T33)) → permE_out_ga(.(T24, T25), .(T26, T33))
APP2B_IN_GGA(.(T105, T106), T107, .(T105, X183)) → APP2B_IN_GGA(T106, T107, X183)
permE_in_ga(.(T24, T25), .(T26, T27)) → U4_ga(T24, T25, T26, T27, app1A_in_aaag(X45, T26, X46, T25))
app1A_in_aaag(.(T50, X94), T52, X95, .(T50, T51)) → U1_aaag(T50, X94, T52, X95, T51, app1A_in_aaag(X94, T52, X95, T51))
app1A_in_aaag([], T60, T61, .(T60, T61)) → app1A_out_aaag([], T60, T61, .(T60, T61))
U1_aaag(T50, X94, T52, X95, T51, app1A_out_aaag(X94, T52, X95, T51)) → app1A_out_aaag(.(T50, X94), T52, X95, .(T50, T51))
U4_ga(T24, T25, T26, T27, app1A_out_aaag(X45, T26, X46, T25)) → permE_out_ga(.(T24, T25), .(T26, T27))
permE_in_ga(.(T24, T25), .(T26, T33)) → U5_ga(T24, T25, T26, T33, app1A_in_aaag(T31, T26, T32, T25))
U5_ga(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → U6_ga(T24, T25, T26, T33, app2C_in_ggga(T24, T31, T32, X11))
app2C_in_ggga(T87, T88, T89, .(T87, X153)) → U3_ggga(T87, T88, T89, X153, app2B_in_gga(T88, T89, X153))
app2B_in_gga(.(T105, T106), T107, .(T105, X183)) → U2_gga(T105, T106, T107, X183, app2B_in_gga(T106, T107, X183))
app2B_in_gga([], T113, T113) → app2B_out_gga([], T113, T113)
U2_gga(T105, T106, T107, X183, app2B_out_gga(T106, T107, X183)) → app2B_out_gga(.(T105, T106), T107, .(T105, X183))
U3_ggga(T87, T88, T89, X153, app2B_out_gga(T88, T89, X153)) → app2C_out_ggga(T87, T88, T89, .(T87, X153))
U6_ga(T24, T25, T26, T33, app2C_out_ggga(T24, T31, T32, X11)) → permE_out_ga(.(T24, T25), .(T26, T33))
U5_ga(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → U7_ga(T24, T25, T26, T33, app2C_in_ggga(T24, T31, T32, T65))
U7_ga(T24, T25, T26, T33, app2C_out_ggga(T24, T31, T32, T65)) → U8_ga(T24, T25, T26, T33, permE_in_ga(T65, T33))
permE_in_ga(.(T125, T126), .(T125, T127)) → U9_ga(T125, T126, T127, app2D_in_ga(T126, X11))
app2D_in_ga(T131, T131) → app2D_out_ga(T131, T131)
U9_ga(T125, T126, T127, app2D_out_ga(T126, X11)) → permE_out_ga(.(T125, T126), .(T125, T127))
permE_in_ga(.(T125, T126), .(T125, T127)) → U10_ga(T125, T126, T127, app2D_in_ga(T126, T128))
U10_ga(T125, T126, T127, app2D_out_ga(T126, T128)) → U11_ga(T125, T126, T127, permE_in_ga(T128, T127))
permE_in_ga([], []) → permE_out_ga([], [])
U11_ga(T125, T126, T127, permE_out_ga(T128, T127)) → permE_out_ga(.(T125, T126), .(T125, T127))
U8_ga(T24, T25, T26, T33, permE_out_ga(T65, T33)) → permE_out_ga(.(T24, T25), .(T26, T33))
APP2B_IN_GGA(.(T105, T106), T107, .(T105, X183)) → APP2B_IN_GGA(T106, T107, X183)
APP2B_IN_GGA(.(T105, T106), T107) → APP2B_IN_GGA(T106, T107)
From the DPs we obtained the following set of size-change graphs:
APP1A_IN_AAAG(.(T50, X94), T52, X95, .(T50, T51)) → APP1A_IN_AAAG(X94, T52, X95, T51)
permE_in_ga(.(T24, T25), .(T26, T27)) → U4_ga(T24, T25, T26, T27, app1A_in_aaag(X45, T26, X46, T25))
app1A_in_aaag(.(T50, X94), T52, X95, .(T50, T51)) → U1_aaag(T50, X94, T52, X95, T51, app1A_in_aaag(X94, T52, X95, T51))
app1A_in_aaag([], T60, T61, .(T60, T61)) → app1A_out_aaag([], T60, T61, .(T60, T61))
U1_aaag(T50, X94, T52, X95, T51, app1A_out_aaag(X94, T52, X95, T51)) → app1A_out_aaag(.(T50, X94), T52, X95, .(T50, T51))
U4_ga(T24, T25, T26, T27, app1A_out_aaag(X45, T26, X46, T25)) → permE_out_ga(.(T24, T25), .(T26, T27))
permE_in_ga(.(T24, T25), .(T26, T33)) → U5_ga(T24, T25, T26, T33, app1A_in_aaag(T31, T26, T32, T25))
U5_ga(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → U6_ga(T24, T25, T26, T33, app2C_in_ggga(T24, T31, T32, X11))
app2C_in_ggga(T87, T88, T89, .(T87, X153)) → U3_ggga(T87, T88, T89, X153, app2B_in_gga(T88, T89, X153))
app2B_in_gga(.(T105, T106), T107, .(T105, X183)) → U2_gga(T105, T106, T107, X183, app2B_in_gga(T106, T107, X183))
app2B_in_gga([], T113, T113) → app2B_out_gga([], T113, T113)
U2_gga(T105, T106, T107, X183, app2B_out_gga(T106, T107, X183)) → app2B_out_gga(.(T105, T106), T107, .(T105, X183))
U3_ggga(T87, T88, T89, X153, app2B_out_gga(T88, T89, X153)) → app2C_out_ggga(T87, T88, T89, .(T87, X153))
U6_ga(T24, T25, T26, T33, app2C_out_ggga(T24, T31, T32, X11)) → permE_out_ga(.(T24, T25), .(T26, T33))
U5_ga(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → U7_ga(T24, T25, T26, T33, app2C_in_ggga(T24, T31, T32, T65))
U7_ga(T24, T25, T26, T33, app2C_out_ggga(T24, T31, T32, T65)) → U8_ga(T24, T25, T26, T33, permE_in_ga(T65, T33))
permE_in_ga(.(T125, T126), .(T125, T127)) → U9_ga(T125, T126, T127, app2D_in_ga(T126, X11))
app2D_in_ga(T131, T131) → app2D_out_ga(T131, T131)
U9_ga(T125, T126, T127, app2D_out_ga(T126, X11)) → permE_out_ga(.(T125, T126), .(T125, T127))
permE_in_ga(.(T125, T126), .(T125, T127)) → U10_ga(T125, T126, T127, app2D_in_ga(T126, T128))
U10_ga(T125, T126, T127, app2D_out_ga(T126, T128)) → U11_ga(T125, T126, T127, permE_in_ga(T128, T127))
permE_in_ga([], []) → permE_out_ga([], [])
U11_ga(T125, T126, T127, permE_out_ga(T128, T127)) → permE_out_ga(.(T125, T126), .(T125, T127))
U8_ga(T24, T25, T26, T33, permE_out_ga(T65, T33)) → permE_out_ga(.(T24, T25), .(T26, T33))
APP1A_IN_AAAG(.(T50, X94), T52, X95, .(T50, T51)) → APP1A_IN_AAAG(X94, T52, X95, T51)
APP1A_IN_AAAG(.(T50, T51)) → APP1A_IN_AAAG(T51)
From the DPs we obtained the following set of size-change graphs:
PERME_IN_GA(.(T24, T25), .(T26, T33)) → U5_GA(T24, T25, T26, T33, app1A_in_aaag(T31, T26, T32, T25))
U5_GA(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → U7_GA(T24, T25, T26, T33, app2C_in_ggga(T24, T31, T32, T65))
U7_GA(T24, T25, T26, T33, app2C_out_ggga(T24, T31, T32, T65)) → PERME_IN_GA(T65, T33)
PERME_IN_GA(.(T125, T126), .(T125, T127)) → U10_GA(T125, T126, T127, app2D_in_ga(T126, T128))
U10_GA(T125, T126, T127, app2D_out_ga(T126, T128)) → PERME_IN_GA(T128, T127)
permE_in_ga(.(T24, T25), .(T26, T27)) → U4_ga(T24, T25, T26, T27, app1A_in_aaag(X45, T26, X46, T25))
app1A_in_aaag(.(T50, X94), T52, X95, .(T50, T51)) → U1_aaag(T50, X94, T52, X95, T51, app1A_in_aaag(X94, T52, X95, T51))
app1A_in_aaag([], T60, T61, .(T60, T61)) → app1A_out_aaag([], T60, T61, .(T60, T61))
U1_aaag(T50, X94, T52, X95, T51, app1A_out_aaag(X94, T52, X95, T51)) → app1A_out_aaag(.(T50, X94), T52, X95, .(T50, T51))
U4_ga(T24, T25, T26, T27, app1A_out_aaag(X45, T26, X46, T25)) → permE_out_ga(.(T24, T25), .(T26, T27))
permE_in_ga(.(T24, T25), .(T26, T33)) → U5_ga(T24, T25, T26, T33, app1A_in_aaag(T31, T26, T32, T25))
U5_ga(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → U6_ga(T24, T25, T26, T33, app2C_in_ggga(T24, T31, T32, X11))
app2C_in_ggga(T87, T88, T89, .(T87, X153)) → U3_ggga(T87, T88, T89, X153, app2B_in_gga(T88, T89, X153))
app2B_in_gga(.(T105, T106), T107, .(T105, X183)) → U2_gga(T105, T106, T107, X183, app2B_in_gga(T106, T107, X183))
app2B_in_gga([], T113, T113) → app2B_out_gga([], T113, T113)
U2_gga(T105, T106, T107, X183, app2B_out_gga(T106, T107, X183)) → app2B_out_gga(.(T105, T106), T107, .(T105, X183))
U3_ggga(T87, T88, T89, X153, app2B_out_gga(T88, T89, X153)) → app2C_out_ggga(T87, T88, T89, .(T87, X153))
U6_ga(T24, T25, T26, T33, app2C_out_ggga(T24, T31, T32, X11)) → permE_out_ga(.(T24, T25), .(T26, T33))
U5_ga(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → U7_ga(T24, T25, T26, T33, app2C_in_ggga(T24, T31, T32, T65))
U7_ga(T24, T25, T26, T33, app2C_out_ggga(T24, T31, T32, T65)) → U8_ga(T24, T25, T26, T33, permE_in_ga(T65, T33))
permE_in_ga(.(T125, T126), .(T125, T127)) → U9_ga(T125, T126, T127, app2D_in_ga(T126, X11))
app2D_in_ga(T131, T131) → app2D_out_ga(T131, T131)
U9_ga(T125, T126, T127, app2D_out_ga(T126, X11)) → permE_out_ga(.(T125, T126), .(T125, T127))
permE_in_ga(.(T125, T126), .(T125, T127)) → U10_ga(T125, T126, T127, app2D_in_ga(T126, T128))
U10_ga(T125, T126, T127, app2D_out_ga(T126, T128)) → U11_ga(T125, T126, T127, permE_in_ga(T128, T127))
permE_in_ga([], []) → permE_out_ga([], [])
U11_ga(T125, T126, T127, permE_out_ga(T128, T127)) → permE_out_ga(.(T125, T126), .(T125, T127))
U8_ga(T24, T25, T26, T33, permE_out_ga(T65, T33)) → permE_out_ga(.(T24, T25), .(T26, T33))
PERME_IN_GA(.(T24, T25), .(T26, T33)) → U5_GA(T24, T25, T26, T33, app1A_in_aaag(T31, T26, T32, T25))
U5_GA(T24, T25, T26, T33, app1A_out_aaag(T31, T26, T32, T25)) → U7_GA(T24, T25, T26, T33, app2C_in_ggga(T24, T31, T32, T65))
U7_GA(T24, T25, T26, T33, app2C_out_ggga(T24, T31, T32, T65)) → PERME_IN_GA(T65, T33)
PERME_IN_GA(.(T125, T126), .(T125, T127)) → U10_GA(T125, T126, T127, app2D_in_ga(T126, T128))
U10_GA(T125, T126, T127, app2D_out_ga(T126, T128)) → PERME_IN_GA(T128, T127)
app1A_in_aaag(.(T50, X94), T52, X95, .(T50, T51)) → U1_aaag(T50, X94, T52, X95, T51, app1A_in_aaag(X94, T52, X95, T51))
app1A_in_aaag([], T60, T61, .(T60, T61)) → app1A_out_aaag([], T60, T61, .(T60, T61))
app2C_in_ggga(T87, T88, T89, .(T87, X153)) → U3_ggga(T87, T88, T89, X153, app2B_in_gga(T88, T89, X153))
app2D_in_ga(T131, T131) → app2D_out_ga(T131, T131)
U1_aaag(T50, X94, T52, X95, T51, app1A_out_aaag(X94, T52, X95, T51)) → app1A_out_aaag(.(T50, X94), T52, X95, .(T50, T51))
U3_ggga(T87, T88, T89, X153, app2B_out_gga(T88, T89, X153)) → app2C_out_ggga(T87, T88, T89, .(T87, X153))
app2B_in_gga(.(T105, T106), T107, .(T105, X183)) → U2_gga(T105, T106, T107, X183, app2B_in_gga(T106, T107, X183))
app2B_in_gga([], T113, T113) → app2B_out_gga([], T113, T113)
U2_gga(T105, T106, T107, X183, app2B_out_gga(T106, T107, X183)) → app2B_out_gga(.(T105, T106), T107, .(T105, X183))
PERME_IN_GA(.(T24, T25)) → U5_GA(T24, app1A_in_aaag(T25))
U5_GA(T24, app1A_out_aaag(T31, T26, T32)) → U7_GA(app2C_in_ggga(T24, T31, T32))
U7_GA(app2C_out_ggga(T65)) → PERME_IN_GA(T65)
PERME_IN_GA(.(T125, T126)) → U10_GA(app2D_in_ga(T126))
U10_GA(app2D_out_ga(T128)) → PERME_IN_GA(T128)
app1A_in_aaag(.(T50, T51)) → U1_aaag(T50, app1A_in_aaag(T51))
app1A_in_aaag(.(T60, T61)) → app1A_out_aaag([], T60, T61)
app2C_in_ggga(T87, T88, T89) → U3_ggga(T87, app2B_in_gga(T88, T89))
app2D_in_ga(T131) → app2D_out_ga(T131)
U1_aaag(T50, app1A_out_aaag(X94, T52, X95)) → app1A_out_aaag(.(T50, X94), T52, X95)
U3_ggga(T87, app2B_out_gga(X153)) → app2C_out_ggga(.(T87, X153))
app2B_in_gga(.(T105, T106), T107) → U2_gga(T105, app2B_in_gga(T106, T107))
app2B_in_gga([], T113) → app2B_out_gga(T113)
U2_gga(T105, app2B_out_gga(X183)) → app2B_out_gga(.(T105, X183))
app1A_in_aaag(x0)
app2C_in_ggga(x0, x1, x2)
app2D_in_ga(x0)
U1_aaag(x0, x1)
U3_ggga(x0, x1)
app2B_in_gga(x0, x1)
U2_gga(x0, x1)
PERME_IN_GA(.(T24, T25)) → U5_GA(T24, app1A_in_aaag(T25))
U5_GA(T24, app1A_out_aaag(T31, T26, T32)) → U7_GA(app2C_in_ggga(T24, T31, T32))
U7_GA(app2C_out_ggga(T65)) → PERME_IN_GA(T65)
PERME_IN_GA(.(T125, T126)) → U10_GA(app2D_in_ga(T126))
U10_GA(app2D_out_ga(T128)) → PERME_IN_GA(T128)
app1A_in_aaag(.(T50, T51)) → U1_aaag(T50, app1A_in_aaag(T51))
app1A_in_aaag(.(T60, T61)) → app1A_out_aaag([], T60, T61)
app2C_in_ggga(T87, T88, T89) → U3_ggga(T87, app2B_in_gga(T88, T89))
app2D_in_ga(T131) → app2D_out_ga(T131)
U1_aaag(T50, app1A_out_aaag(X94, T52, X95)) → app1A_out_aaag(.(T50, X94), T52, X95)
U3_ggga(T87, app2B_out_gga(X153)) → app2C_out_ggga(.(T87, X153))
app2B_in_gga(.(T105, T106), T107) → U2_gga(T105, app2B_in_gga(T106, T107))
app2B_in_gga([], T113) → app2B_out_gga(T113)
U2_gga(T105, app2B_out_gga(X183)) → app2B_out_gga(.(T105, X183))
U10GA1 > app2Cinggga3 > U3ggga2 > U5GA2 > app2Bingga2 > U7GA1 > PERMEINGA1 > app1Ainaaag1 > U1aaag2 > U2gga2 > app2Coutggga1 > app2Boutgga1 > app1Aoutaaag3 > app2Dinga1 > app2Doutga1 > [] > .2
[]=5
app1A_in_aaag_1=3
app2D_in_ga_1=2
app2D_out_ga_1=1
app2B_out_gga_1=5
app2C_out_ggga_1=3
PERME_IN_GA_1=4
U7_GA_1=1
U10_GA_1=3
._2=2
U1_aaag_2=2
app1A_out_aaag_3=0
app2C_in_ggga_3=0
U3_ggga_2=0
app2B_in_gga_2=0
U2_gga_2=2
U5_GA_2=0
app1A_in_aaag(x0)
app2C_in_ggga(x0, x1, x2)
app2D_in_ga(x0)
U1_aaag(x0, x1)
U3_ggga(x0, x1)
app2B_in_gga(x0, x1)
U2_gga(x0, x1)